T:Type, L:T List. null(L)  L = (firstn(||L||-1;L) @ [last(L)]) 

latex

Definitions	hd(l), l[i], ij, last(L), as @ bs, firstn(n;as), null(as), Unit, P  Q, P & Q, P  Q, T, i<j, ||as||, , ij, AB, b, Prop, b, True, x:A. B(x), t  T, A, P  Q, False
Lemmas	false wf, not wf, true wf, bnot wf, assert wf, le wf, le int wf, bool wf, length wf1, lt int wf, assert of le int, bnot of lt int, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, null wf, length zero, not functionality wrt iff, assert of null, firstn wf, append wf, select wf, non neg length, length cons, select cons tl, last wf